invert{-}union($x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $x$ of inl($a$) =$>$ inr $a$  $\mid$ inr($a$) =$>$ inl $a$